forall a: forall b: forall c:
forall Q:a->b:
forall R:b->c:
forall S:b->c:
Q;(R|S) = Q;R|Q;S